$\vdash$  (tt = tt) $\vee$ ($\neg$(tt = tt))